/*
 * TestsuiteRunner.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

/**
 * Runs tests for different input problems and generates an output.
 */

#include <getopt.h>

#include <cassert>

#include <iostream>
#include <fstream>
#include <limits.h>
#include <string>
#include <list>
#include <utility>
#include <vector>

#include <boost/timer.hpp>
#include <boost/filesystem.hpp>

#include "bfr/ClauseSet.hpp"
#include "bfr/DIMACSParser.hpp"
#include "bfr/LPB.hpp"
#include "bfr/lpbCombinatorial/SplittingTree.hpp"
#include "bfr/LPBConversionException.hpp"
#include "bfr/lpbCombinatorial/ExtendedTreeSolver.hpp"
#include "bfr/lpbCombinatorial/MinimumChooser.hpp"

using namespace std;
using namespace bfr;
using boost::timer;
using boost::filesystem::exists;
using boost::filesystem::is_directory;
using boost::filesystem::path;
using boost::filesystem::directory_iterator;

template<class TreeSolverT>
void runTreeSolver(TreeSolverT &minSolver, size_t size,
                      ClauseSet *cs, bool cutTree) {
    // start combinatorial solver
    SplittingTree t(cs, size);
    if (cutTree) {
        t.createTree<true>(true, false);
    }
    else {
        t.createTree<false>(true, false);
    }
    LPB *lpb;
    try {
        lpb = minSolver.solve(&t);
    } catch (const LPBConversionException &e) {
        cout << "Can't convert DNF to LPB. Error message:"
             << endl
             << e.what()
             << endl;
        return;
    }
    // compare result
    ClauseSet *resultSet = lpb->toDNF();
    if (*cs != *resultSet) {
        cout << "Sets are not equal!" << endl;
        cout << *cs << endl;
        cout << *resultSet << endl;
    }
    delete lpb;
    delete resultSet;
}

int main(int argc, char **argv) {
    const string dnfExtension = ".dnf";
    const int maxID = CHAR_MAX;
    static struct option long_options[] = {
            {"help", no_argument, 0, 'h'},
            {"out", required_argument, 0, 'o'},
            {"in", required_argument, 0, 'i'},
            {"recursive", no_argument, 0, 'r'},
            {0, 0, 0, 0}
    };
    DIMACSParser parser;
    int index = 0;
    int c;
    string outFile;
    string inDir;
    ExtendedTreeSolver<MinimumChooser> minRepairSolver;
    bool recursive = false;
    while ((c = getopt_long(argc, argv, "ho:i:",
            long_options, &index)) != -1) {
        switch (c) {
        case 0:
        case 1:
        case 2:
            // should not happen
            break;
        case 'h': {
            cout << "This program runs testmarks for the"
                    " threshold synthesis problem."
                 << endl;
            return 0;
            break;
        }
        case 'o': {
            outFile = optarg;
            break;
        }
        case 'i': {
            inDir = optarg;
            break;
        }
        case 'r': {
            recursive = true;
            break;
        }
        }
    }
    if (inDir == "") {
        cerr << "You haven't specified an input directory."
             << endl;
        return 1;
    }
    path inPath(inDir);
    if (!exists(inPath)) {
        cerr << "File \"" << inDir << "\" does not exist."
             << endl;
        return 1;
    }
    if (!is_directory(inPath)) {
        cerr << "Input path \"" << inDir << "\" is not a directory."
             << endl;
        return 1;
    }
    path outPath(outFile);
    list<path> waitingDirs;
    waitingDirs.push_back(inDir);
    list<string> dirs;
    list<list<pair<ClauseSet*, size_t> > > instances;
    while (!waitingDirs.empty()) {
        path next = waitingDirs.front();
        waitingDirs.pop_front();
        assert(is_directory(next));
        dirs.push_back(next.string());
        list<pair<ClauseSet*, size_t>> clauses;

        directory_iterator end;
        for (directory_iterator it(next); it != end; ++it) {
            path p = (*it).path();
            if (is_directory(p)) {
                waitingDirs.push_back(p);
            }
            else {
                if (p.extension().string() == dnfExtension) {
                    ClauseSet *cs = 0;
                    try {
                        ifstream in;
                        in.open(p.c_str());
                        cs = parser.parse(in);
                        in.close();
                        runTreeSolver(minRepairSolver, parser.getVariableCount(), cs, false);
                        if (cs != 0)
                            delete cs;
                    } catch (string &e) {
                        cerr << "Error parsing file \"" << p << "\":" << endl;
                        cerr << e << endl;
                    }
                }
            }
        }
        instances.push_back(clauses);
    }
    return 0;
}
